Multiprocess systems, including grid systems, multiprocessors and multicorecomputers, incorporate a variety of specialized hardware and softwaremechanisms, which speed computation, but result in complex memory behavior. Asa consequence, the possible outcomes of a concurrent program can be unexpected.A memory consistency model is a description of the behaviour of such a system.Abstract memory consistency models aim to capture the concrete implementationsand architectures. Therefore, formal specification of the implementation orarchitecture is necessary, and proofs of correspondence between the abstractand the concrete models are required. This paper provides a case study of this process. We specify a new model,partition consistency, that generalizes many existing consistency models. Aconcrete message-passing network model is also specified. Implementations ofpartition consistency on this network model are then presented and provedcorrect. A middle level of abstraction is utilized to facilitate the proofs.All three levels of abstraction are specified using the same framework. Thepaper aims to illustrate a general methodology and techniques for specifyingmemory consistency models and proving the correctness of their implementations.
展开▼
